weakSendDoApplyR{$a:ut2, $tg:ut2}
weakSendDoApplyR(T; t; l; ds; f)
== weakPrecondSendR2{$a:ut2, $tg:ut2}
== weakPrecondSendR2(T; t; *1*; l; ds; (s.can-apply(f;s)); (s,v. do-apply(f;s))) 

latex

Definitions

weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f), *1*, can-apply(f;x), x.A(x), do-apply(f;x)